function TestCtrl($scope) {

  $scope.expressionR = {
    kind: 'variable',
    operator: 'R',
    arguments: [],
    dummies: []
  }
  $scope.expressionS = {
    kind: 'variable',
    operator: 'S',
    arguments: [],
    dummies: []
  }
  $scope.expressionRandS = {
    kind: 'binary_connective',
    operator: 'and',
    arguments: [$scope.expressionR, $scope.expressionS],
    dummies: []
  }
  $scope.expressiona = {
    kind:'variable',
    operator:'a',
    arguments:[],
    dummies:[]
  }
  $scope.expressionAllxp = {
    kind:'quantifier',
    operator:'for_all',
    arguments:[{
      kind:'variable',
      operator:'p',
      arguments:[],
      dummies:[]
    }],
    dummies:[{
      kind:'variable',
      operator:'x',
      arguments:[],
      dummies:[]
    }]
  }
  $scope.expressionT = {
    kind: 'variable',
    operator: 'T',
    arguments: [],
    dummies: []
  }
  $scope.expressionU = {
    kind: 'variable',
    operator: 'U',
    arguments: [],
    dummies: []
  }

  $scope.sampleControlLanguage = BASE_CONTROL_LANGUAGE;
  $scope.sampleControlModel = BASE_CONTROL_MODEL;
  $scope.sampleControlLanguage.operators['scoper'] = {
    kind:'prefix_function',
    typing:[{
      arguments:['integer'],
      dummies:[],
      output:'integer'
    }]
  } 
  $scope.sampleControlModel.evaluation_rules['scoper'] = {
    format:'definition',
    content:{
      kind:'ranged_function',
      operator:'max',
      arguments:[{
        kind:'binary_relation',
        operator:'less_than',
        arguments:[{
          kind:'variable',
          operator:'k',
          arguments:[],
          dummies:[],
          type: 'integer'
        },{
          kind:'variable',
          operator:'n',
          arguments:[],
          dummies:[],
          type: 'integer'
        }],
        dummies:[],
        type: 'boolean'
      },{
        kind:'binary_relation',
        operator:'less_than',
        arguments:[{
          kind:'prefix_function',
          operator:'indentation',
          arguments:[{
            kind:'variable',
            operator:'k',
            arguments:[],
            dummies:[],
            type: 'integer'
          }],
          dummies:[],
          type: 'integer'
        },{
          kind:'prefix_function',
          operator:'indentation',
          arguments:[{
            kind:'variable',
            operator:'n',
            arguments:[],
            dummies:[],
            type: 'integer'
          }],
          dummies:[],
          type: 'integer'
        }],
        dummies:[],
        integer: 'boolean'
      }],
      dummies:[{
        kind:'variable',
        operator:'k',
        arguments:[],
        dummies:[],
        type: 'integer'
      }]
    },
    variables:[{
      kind:'variable',
      operator:'n',
      arguments:[],
      dummies:[]
    }],
    description:'The most recent line (not including n) in whose scope line n is'
  }

  $scope.sampleWidget = {
    assumptions: [],
    results: [{
      kind: 'variable',
      operator: 'p',
      arguments: [],
      dummies: []
    }],
    language: BASE_STUDENT_LANGUAGE,
    general_messages: DEFAULT_ERROR_MESSAGES,
    line_templates: [{
      name:'and_introduce',
      reader_view:[{
        format:'phrase',
        content:'from'
      },{
        format:'expression',
        content: {
          expression: $scope.expressionR,
          substitutions:[],
          type:'boolean'
        }
      },{
        format:'phrase',
        content:'and'
      },{
        format:'expression',
        content:{
          expression: $scope.expressionS,
          substitutions:[],
          type:'boolean'
        }
      },{
        format:'phrase',
        content:'have'
      },{
        format:'expression',
        content:{
          expression: $scope.expressionRandS,
          substitutions:[],
          type:'boolean'
        }
      }],
      antecedents:[{
        expression: $scope.expressionR,
        substitutions:[],
        type:'boolean'
      },{
        expression: $scope.expressionS,
        substitutions:[],
        type:'boolean'
      }],
      results:[{
        expression: $scope.expressionRandS,
        substitutions:[],
        type:'boolean'
      }],
      variables:[],
      error:[]
    }, {
      name:'for_all_introduce',
      reader_view:[{
        format:'expression',
        content:{
          expression: $scope.expressiona,
          substitutions:[],
          type:'element',
          kind: 'variable'
        }
      },{
        format:'phrase',
        content:'arbitrary'
      },{
        format:'phrase',
        content:'hence'
      },{
        format:'expression',
        content:{
          expression: $scope.expressionAllxp,
          substitutions:[],
          type:'boolean'
        }
      }],
      antecedents:[{
        expression:{
          kind:'variable',
          operator:'p',
          arguments:[],
          dummies:[]
        },
        substitutions:[{
          'x': $scope.expressiona
        }],
        type:'boolean'
      }],
      results:[{
        expression: $scope.expressionAllxp,
        substitutions:[],
        type:'boolean'
      }],
      variables: [$scope.expressiona],
      error:[]
    }, {
      name:'and_introduce_e4',
      reader_view:[{
        format:'phrase',
        content:'from'
      },{
        format:'expression',
        content:{
          expression: $scope.expressionT,
          substitutions:[],
          type:'boolean'
        }
      },{
        format:'phrase',
        content:'and'
      },{
        format:'expression',
        content:{
          expression: $scope.expressionU,
          substitutions:[],
          type:'boolean'
        }
      },{
        format:'phrase',
        content:'have'
      },{
        format:'expression',
        content:{
          expression: $scope.expressionRandS,
          substitutions:[],
          type:'boolean'
        }
      }],
      antecedents: [],
      results: [],
      variables: [],
      error:[[{
        format:'string',
        content:'The conclusion you are allowed to make here is \'From '
      },{
        format:'expression',
        content:{
          expression: $scope.expressionT,
          substitutions:[],
          type:'boolean'
        }
      },{
        format:'string',
        content:' and '
      },{
        format:'expression',
        content:{
          expression: $scope.expressionU,
          substitutions:[],
          type:'boolean'
        }
      },{
        format:'string',
        content:' we have '
      },{
        format:'expression',
        content:{
          expression:{
            kind:'binary_connective',
            operator:'and',
            arguments:[$scope.expressionT, $scope.expressionU],
            dummies:[]
          },
          substitutions:[],
          type:'boolean'
        }
      },{
        format:'string',
        content:'\'.'
      }]]
    }],
    vocabulary: BASE_VOCABULARY,
    mistake_table: [{
      name: 'variables',
      entries: [{
        name:'incorrect_variable_forall',
        occurs: assignTypesToExpression(
          parser.parse(
            'template(n)=\'for_all_introduce\'&entry(1,variables(n))!=entry(1,variables(scoper(n-1)))', 'expression'),
            ['boolean'], $scope.sampleControlLanguage, ['constant', 'variable'])[0].typedExpression,
        message:[[{
          format:'string',
          content:'We originally took '
        },{
          format:'expression',
          content: assignTypesToExpression(
            parser.parse(
              'entry(1,variables(scoper(n-1)))', 'expression'),
              ['formula'], $scope.sampleControlLanguage, ['constant', 'variable'])[0].typedExpression
        }, {
          format:'string',
          content:' as our arbitrary variable so this, rather than '
        },{
          format:'expression',
          content:{
            operator:'variables',
            kind:'prefix_function',
            arguments:[{
              operator:'n',
              kind:'variable',
              arguments:[],
              dummies:[],
              type:'integer'
            }],
            dummies:[],
            type:'set_of_formulas'
          }
        },{
          format:'string',
          content:', needs to be the one that we quantify out over.'
        }]]
      }]
    }, {
      name: 'target',
      entries: [{
        name:'last_line_indented_assumption',
        occurs: assignTypesToExpression(
          parser.parse(
            'n=num_lines()&indentation(n)>0&template(scoper(n))!=\'given\'', 'expression'),
            ['boolean'], $scope.sampleControlLanguage, ['constant', 'variable'])[0].typedExpression,
        message:[[{
          format:'string',
          content:'The last line of a proof should not be indented; you need to prove that the given formulas holds just from the original assumptions, not the additional assumption of '
        },{
          format:'expression',
          content: assignTypesToExpression(
            parser.parse(
              'entry(1,results(scoper(n)))', 'expression'),
              ['formula'], $scope.sampleControlLanguage, ['constant', 'variable'])[0].typedExpression
        }, {
          format:'string',
          content:'.'
        }]]
      }]
    }],
    control_language: $scope.sampleControlLanguage,
    control_model: $scope.sampleControlModel
  }


  $scope.tests = {
    'match_expression_1': {
      expected: 'p:A(x), q:t',
      actual: displayExpressionDictionary(
        matchExpression(
          parser.parse('A(x)&t', 'expression'), 
          parser.parse('p&q', 'expression'), {}, BASE_STUDENT_LANGUAGE.kinds
        ), 
        BASE_STUDENT_LANGUAGE.operators
      )
    },
    'match_expression_2': {
      error: 'This line could not be identified as valid - please check the list of acceptable lines.',
      actual: function() {
        matchExpression(
          parser.parse('A(x)&t', 'expression'), 
          parser.parse('p&q', 'expression'), {q: parser.parse('s', 'expression')},
          BASE_STUDENT_LANGUAGE.kinds
        )
      }
    },
    'match_expression_3': {
      expected: 'p:R(y), x:y',
      actual: displayExpressionDictionary(
        matchExpression(
          parser.parse('$y.R(y)', 'expression'), 
          parser.parse( '$x.p', 'expression'), {}, BASE_STUDENT_LANGUAGE.kinds
        ), 
        BASE_STUDENT_LANGUAGE.operators
      )
    },
    'substitute_into_expression_1': {
      expected: displayExpression(parser.parse('(B(x)<=>q)&A(y+2,y+2)', 'expression'), BASE_STUDENT_LANGUAGE.operators),
      actual: displayExpression(
        substituteIntoExpression(parser.parse('p&A(x,x)', 'expression'), {
          p: parser.parse('B(x)<=>q', 'expression'),
          x: parser.parse('y+2', 'expression')
        }), BASE_STUDENT_LANGUAGE.operators)
    },
    'substitute_into_expression_2': {
      expected: displayExpression(parser.parse('@y.y=22', 'expression'), BASE_STUDENT_LANGUAGE.operators),
      actual: displayExpression(
        substituteIntoExpression(parser.parse('@y.y=z', 'expression'), {
          y: parser.parse('x', 'expression'),
          z: parser.parse('22', 'expression')
        }), BASE_STUDENT_LANGUAGE.operators)
    },
    'instantiate_expression': {
      expected: displayExpression(parser.parse('@x.x=22|(p=>p)', 'expression'), BASE_STUDENT_LANGUAGE.operators),
      actual: displayExpression(
        instantiateExpression(
          parser.parse('@y.y=z|p', 'expression'), {
            y: parser.parse('x', 'expression'),
            z: parser.parse('22', 'expression'),
            p: parser.parse('p=>p', 'expression')
        }), BASE_STUDENT_LANGUAGE.operators)
    },
    'compute_expression_from_template': {
      expected: displayExpression(parser.parse('B(2-2)', 'expression'), BASE_STUDENT_LANGUAGE.operators),
      actual: displayExpression(
        computeExpressionFromTemplate(
          parser.parse('p[x->a]', 'booleanTemplate'), {
          p: parser.parse('B(y)', 'expression'),
          x: parser.parse('y', 'expression'),
          a: parser.parse('2-2', 'expression')
        }), BASE_STUDENT_LANGUAGE.operators)
    },
    'render_line_message': {
      error: 'The conclusion you are allowed to make here is \'From x=y and A2(x,y) we have (x=y)&A2(x,y)\'.',
      actual: function() {
          renderLineMessages($scope.sampleWidget.line_templates[2].error, {
          T: parser.parse('x=y', 'expression'),
          U: parser.parse('A2(x,y)', 'expression')
        }, BASE_STUDENT_LANGUAGE.operators)
      }
    },
    'match_line_to_template_1': {
      expected: JSON.stringify({
        R: parser.parse('A(x,y)', 'expression'),
        S: parser.parse('A(y,z)', 'expression')
      }),
      actual: JSON.stringify(
        matchLineToTemplate(
          parseLine('from A(x,y) and A(y,z) we have A(x,y)&A(y,z)', BASE_STUDENT_LANGUAGE.operators, BASE_VOCABULARY).results[0],
          $scope.sampleWidget.line_templates[0].reader_view, BASE_STUDENT_LANGUAGE.kinds))
    },
    'match_line_to_template_2': {
      expected: JSON.stringify({
        a: parser.parse('z', 'expression'),
        p: parser.parse('x=2', 'expression'),
        x: parser.parse('x', 'expression')
      }),
      actual: JSON.stringify(
        matchLineToTemplate(
          parseLine('z was arbitrary so @x.x=2', BASE_STUDENT_LANGUAGE.operators, BASE_VOCABULARY).results[0],
          $scope.sampleWidget.line_templates[1].reader_view, BASE_STUDENT_LANGUAGE.kinds))
    },
    'match_line_to_template_3': {
      error: 'This line could not be identified as valid - please check the list of acceptable lines.',
      actual: function() {
        matchLineToTemplate(
          parseLine('from p and q we have q&p', BASE_STUDENT_LANGUAGE.operators, BASE_VOCABULARY).results[0],
          $scope.sampleWidget.line_templates[0].reader_view, BASE_STUDENT_LANGUAGE.kinds)
      } 
    },
    'match_line_to_template_4': {
      error: 'This line could not be identified as valid - please check the list of acceptable lines.',
      actual: function() {
        matchLineToTemplate(
          parseLine('z was arbitrary from @x.x=2', BASE_STUDENT_LANGUAGE.operators, BASE_VOCABULARY).results[0],
          $scope.sampleWidget.line_templates[1].reader_view, BASE_STUDENT_LANGUAGE.kinds)
      }
    },
    'build_line_1': {
      expected: JSON.stringify({
        template: 'and_introduce',
        elements: {R: 'a|b', S: 'c<=>d'},
        antecedents: 'a|b, c<=>d',
        results: '(a|b)&(c<=>d)',
        variables: '',
        indentation: 2,
        text: '    from a|b and c<=>d have (a|b) & (c<=>d)'
      }),
      actual: JSON.stringify(
        displayLine(
          buildLine(
            '    from a|b and c<=>d have (a|b) & (c<=>d)', 
            $scope.sampleWidget.line_templates, BASE_STUDENT_LANGUAGE, BASE_VOCABULARY
          ), BASE_STUDENT_LANGUAGE.operators
        )
      )
    },
    'build_line_2': {
      error: 'In a line of this form, your x+2 should be a variable.',
      actual: function() {
        buildLine('x+2 was arbitrary so @y.p', $scope.sampleWidget.line_templates, BASE_STUDENT_LANGUAGE, BASE_VOCABULARY)
      }
    },
    'build_line_3': {
      error: 'We could not identify either of \'fromj\' or \'p\' as words; please make sure you are using vocabulary from the given list, and don\'t have two consecutive expressions.',
      actual: function() {
        buildLine('fromj p we have q', $scope.sampleWidget.line_templates, BASE_STUDENT_LANGUAGE, BASE_VOCABULARY)
      }
    },
    'build_line_4': {
      error: 'The operator A could not be identified.',
      actual: function() {
        buildLine('from A(x) and A(y) we have A(x)&A(z)', $scope.sampleWidget.line_templates, BASE_STUDENT_LANGUAGE, BASE_VOCABULARY)
      }
    },
    'build_line_5': {
      error: 'This line could not be identified as valid - please check the list of acceptable lines.',
      actual: function() {
        buildLine('Hence A=>x=3', $scope.sampleWidget.line_templates, BASE_STUDENT_LANGUAGE, BASE_VOCABULARY)
      }
    },
    'build_line_6': {
      error: 'The conclusion you are allowed to make here is \'From a<b and b<c we have (a<b)&(b<c)\'.',
      actual: function() {
        buildLine('from a<b and b<c we have a<b & b<d', $scope.sampleWidget.line_templates, BASE_STUDENT_LANGUAGE, BASE_VOCABULARY)
      }
    },
    'build_proof_1': {
      expected: JSON.stringify([{
        template: 'for_all_introduce',
        elements: {a: 'a', p: 'R', 'x': 'y'},
        antecedents: 'R',
        results: '@y.R',
        variables: 'a',
        indentation: 0,
        text: 'a was arbitrary thus @y.R'
      }, {
        template: 'and_introduce',
        elements: {R: 'p', S: '@y.R'},
        antecedents: 'p, @y.R',
        results: 'p&(@y.R)',
        variables: '',
        indentation: 1,
        text: '  from p and @y.R have p&@y.R'
      }]),
      actual: JSON.stringify(
        displayProof(
          buildProof('a was arbitrary thus @y.R\n  from p and @y.R have p&@y.R', $scope.sampleWidget), 
          BASE_STUDENT_LANGUAGE.operators
        )
      )
    },
    'build_proof_2': {
      expected: 'The conclusion you are allowed to make here is \'From a and b we have a&b\'.',
      actual: buildProof('from a and b we have a&b\nfrom a and b we have b&a', $scope.sampleWidget).failure
    },
    'evaluate_1': {
      expected: 4,
      actual: evaluate(
        assignTypesToExpression(
          parser.parse('2+2', 'expression'), ['integer'], BASE_CONTROL_LANGUAGE
        )[0].typedExpression, {}, BASE_CONTROL_MODEL, {}, {})
    },
    'evaluate_2': {
      expected: true,
      actual: evaluate(
        assignTypesToExpression(
          parser.parse('y?z', 'expression'), ['boolean'], BASE_CONTROL_LANGUAGE
        )[0].typedExpression, 
        {
          x: "a", 
          y: parser.parse('p&q', 'expression'), 
          z: [parser.parse('$x.p', 'expression'), parser.parse('p&q', 'expression')]
        }, BASE_CONTROL_MODEL, {}, {})
    },
    'evaluate_3': {
      expected: true,
      actual: evaluate(
        assignTypesToExpression(
          parser.parse('x=\'a\'', 'expression'), ['boolean'], BASE_CONTROL_LANGUAGE
        )[0].typedExpression, 
        {
          x: '\'a\'', 
          y: parser.parse('p&q', 'expression'), 
          z: [parser.parse('$x.p', 'expression'), parser.parse('p&q', 'expression')]
        }, BASE_CONTROL_MODEL, {}, {})
    },
    'evaluate_4': {
      expected: 7,
      actual: evaluate(assignTypesToExpression(
          parser.parse('max{n<10|~$x<10.$y<10.(x>1&y>1&x*y=n)}', 'expression'), ['integer'], BASE_CONTROL_LANGUAGE
        )[0].typedExpression, {}, BASE_CONTROL_MODEL, {}, {})
    },
    'evaluate_5': {
      expected: 8,
      actual: evaluate(assignTypesToExpression(
          parser.parse('min{n<20|n>1&~@x<5.~x*x*x=n}', 'expression'), ['integer'], BASE_CONTROL_LANGUAGE
        )[0].typedExpression, {}, BASE_CONTROL_MODEL, {}, {})
    },
    'evaluate_6': {
      expected: 'r&s, s',
      actual: displayExpressionArray(
        evaluate(
          assignTypesToExpression(
            parser.parse('antecedents(2)', 'expression'), ['set_of_formulas'],
            BASE_CONTROL_LANGUAGE
          )[0].typedExpression, {}, BASE_CONTROL_MODEL, {
            proof: buildProof('from r and s we have r&s\nfrom r&s and s we have (r&s)&s', $scope.sampleWidget)
          }, {}
        ), BASE_CONTROL_LANGUAGE.operators
      )
    },
    'evaluate_7': {
      expected: 1,
      actual: evaluate(
        assignTypesToExpression(
          parser.parse('scoper(num_lines())', 'expression'), ['integer'],
          $scope.sampleWidget.control_language
        )[0].typedExpression, {}, $scope.sampleWidget.control_model, {
          proof: buildProof('from r and s we have r&s\n  from r&s and s we have (r&s)&s', $scope.sampleWidget)
        }, {}
      )
    },
    'evaluate_8': {
      expected: false,
      actual: evaluate($scope.sampleWidget.mistake_table[0].entries[0].occurs, {n: 3}, $scope.sampleWidget.control_model, {
        proof: buildProof('a was arbitrary hence @x.p\n  from p and q we have p&q\n  a was arbitrary hence @x.q', $scope.sampleWidget)
      }, {})
    },
    'instantiate_control_message_1': {
      error: 'We originally took a as our arbitrary variable so this, rather than b, needs to be the one that we quantify out over.',
      actual: function() {
        renderControlMessage($scope.sampleWidget.mistake_table[0].entries[0], '', 2, $scope.sampleWidget.control_model, {
          proof: buildProof('a was arbitrary hence @x.p\n  from p and q we have p&q\n  b was arbitrary hence @x.q', $scope.sampleWidget)
        }, BASE_STUDENT_LANGUAGE.operators)
      }
    },
    'instantiate_control_message_2': {
      error: 'The last line of a proof should not be indented; you need to prove that the given formulas holds just from the original assumptions, not the additional assumption of @x.p.',
      actual: function() {
        renderControlMessage($scope.sampleWidget.mistake_table[1].entries[0], '', 1, $scope.sampleWidget.control_model, {
          proof: buildProof('a was arbitrary hence @x.p\n  from p and q we have p&q', $scope.sampleWidget)
        }, BASE_STUDENT_LANGUAGE.operators)
      }
    },
    'instantiate_control_message_3': {
      error: 'This line contains a mistake in its target (with code last_line_indented_assumption).',
      actual: function() {
        renderControlMessage($scope.sampleWidget.mistake_table[1].entries[0], 'target', 0, $scope.sampleWidget.control_model, {
          proof: buildProof('a was arbitrary hence @x.p\n  from p and q we have p&q', $scope.sampleWidget)
        }, BASE_STUDENT_LANGUAGE.operators)
      }
    },
    'check_proof_1': {
      expected: true,
      actual: checkProof(
        buildProof(
          'from p and q we have p&q\nfrom p and p&q we have p&(p&q)', $scope.sampleWidget
        ), $scope.sampleWidget)
    },
    'check_proof_2': {
      expected: JSON.stringify({
        failure:'The last line of a proof should not be indented; you need to prove that the given formulas holds just from the original assumptions, not the additional assumption of p&q.',
        line:1
      }),
      actual: JSON.stringify(checkProof(
        buildProof(
          'from p and q we have p&q\n  from p and p&q we have p&(p&q)', $scope.sampleWidget
        ), $scope.sampleWidget))
    },
    'check_proof_3': {
      expected: JSON.stringify({
        failure: 'We originally took a as our arbitrary variable so this, rather than b, needs to be the one that we quantify out over.',
        line:2
      }),
      actual: JSON.stringify(checkProof(
        buildProof(
          'a was arbitrary hence @x.p\n  from p and q we have p&q\n  b was arbitrary hence @x.q', $scope.sampleWidget
        ), $scope.sampleWidget))
    }
  };

  $scope.testResults = [];
  for (var key in $scope.tests) {
    $scope.testResults.push({name: key, expected: 'passed'});
    if ($scope.tests[key].hasOwnProperty('error')) {
      try {
        $scope.tests[key].actual();
        $scope.testResults[$scope.testResults.length-1].expected = 'An error should have occurred and did not.'
      }
        catch(err) {
          var actual = renderError(err, DEFAULT_ERROR_MESSAGES, BASE_STUDENT_LANGUAGE);
          if (actual !== $scope.tests[key].error) {
            $scope.testResults[$scope.testResults.length-1].expected =  $scope.tests[key].error;
            $scope.testResults[$scope.testResults.length-1].actual =  actual;    
          }
        }
    } else {
      if ($scope.tests[key].expected !== $scope.tests[key].actual) {
        $scope.testResults[$scope.testResults.length-1].expected =  $scope.tests[key].expected;
        $scope.testResults[$scope.testResults.length-1].actual =  $scope.tests[key].actual;      
      }
    }
  }
}
